Nuprl Lemma : fpf-trivial-subtype-set
0,22
postcript
pdf
A
:Type,
P
:(
A
Prop),
f
:
a
:{
a
:
A
|
P
(
a
) } fp
Type.
f
a
:
A
fp
Type
latex
Definitions
t
T
,
Prop
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
.
t
(
x
)
Lemmas
fpf
wf
,
subtype-fpf3
,
strong-subtype-set3
,
strong-subtype-self
origin
A:Type, P:(A
Prop), f:a:{a:A| P(a) } fp Type. f 
a:A fp Type A:Type, P:(AProp), f:a:{a:A| P(a) } fp Type. f a:A fp Type Tx:A. B(x)
Q
x. t(x)